import Data.List
import Text.Show.Functions
import LambdaCombinatorsSample
    
-- Free Variables
freeVar :: Expr -> [String]
freeVar (Var x) = [x]
freeVar (App f e) = freeVar f `union` freeVar e
freeVar (Lam x e) = delete x $ freeVar e

-- Variable substitution
subst :: Expr -> String -> Expr -> Expr
subst var@(Var y) x e | y == x = e
                      | otherwise = var
subst (App f a) x e = App (subst f x e) (subst a x e)
subst lam@(Lam y a) x e | y == x = lam
                       | otherwise = Lam y (subst a x e)

varsOf :: Expr -> [String]
varsOf (Var x)   = [x]
varsOf (App f e) = varsOf f `union` varsOf e
varsOf (Lam x e) = varsOf e `union` [x]

fresh :: [String] -> String
fresh = foldl diagonalise "a"
diagonalise  []        []               = "a" 
diagonalise  []      (y:ys) | y == 'a'  = "b"
                             | otherwise = "a" 
diagonalise  s        []                =  s 
diagonalise s@(x:xs) (y:ys) | x /= y    = s  
                             | otherwise = x : diagonalise xs ys

-- alpha - reduction
alpha :: Expr -> [String] -> Expr
alpha (App f e) vars = App (alpha f vars) (alpha e vars)
alpha (Lam x e) vars | x `elem` vars = Lam t $ alpha e' vars
                    | otherwise = Lam x $ alpha e  vars
       where t  = fresh (varsOf e `union` vars)
             e' = subst e x (Var t)
alpha  e       _                       = e

-- beta - reduction
beta :: Expr -> Expr
beta (App (Lam x m) n) = subst (alpha m $ freeVar n) x n
beta (Lam x m) = (Lam x m)
carefulSubst m x n = subst (alpha m $ freeVar n) x n

